
/**
 * A sorted array. Least to greatest
 * 
 */
public class SortedIntegers {
    //@ invariant (\forall int i; 0 < i && i < size; arr[i-1] <= arr[i]);
	//@ invariant (size >= 0);
	//@ invariant (size <= capacity);
	
    private /*@ spec_public @*/ int arr[];
    private /*@ spec_public @*/ int capacity, size = 0;
    
    //@ public normal_behavior
    //@ requires capacity > 0;
    //@ ensures arr.length == capacity;
    //@ assignable this.capacity,this.arr;
    public SortedIntegers(int capacity) {
        this.capacity = capacity;
        this.arr = new int[capacity];
    }
    
    //@ public normal_behavior
    //@ requires size < capacity;
    //@ ensures \old(size)+1 == size;
    //@ assignable arr[*],size;
    //@ also
    //@ public exceptional_behavior
    //@ requires size >= capacity;
    //@ signals_only IndexOutOfBoundsException;
    public void add(int elem){
        if(size < capacity){
        	//put us in right position for adding
        	int i = 0;
        	while(elem > arr[i] && i < size){
        		i++;
        	}
        	
        	//start moving from end of list
			for(int j = size;j > i;j--){
				arr[j]= arr[j-1];
			}	
			arr[i]=elem;
			size++;
			return;
    	}else{
    		throw new IndexOutOfBoundsException("SortedInteger is full");
    	}
    }
    
    //@ public normal_behavior
    //@ requires size > 0;
    //@ requires contains(elem);
    //@ ensures \old(size)-1 == size;
    //@ assignable size, arr[*];
    //@ also
    //@ requires !contains(elem) || size <= 0;
    //@ ensures \old(size)==size;
    public void remove(int elem) {
    	boolean move = false;
    	if(size > 0){
    		for(int i = 0; i < size;i++){
    			if(move){
    				arr[i] = arr[i+1];
    			}else if(arr[i] < elem){
    				continue;
        		}else if(arr[i] > elem){
        			// beacuse we have a sorted array and we have
        			//not accessed if(move) than the elem not exist
        			return;
        		}else if(arr[i]==elem){
        			move = true;
        			i--; // because we increase i with 1 before we access if(move)...
        			size--;// can decraese here because we moving from arr[i+1]...  
        		}
    		}	
    	}
    }
    
    //@ public normal_behavior
    //@ requires size > 0;
    //@ requires (\exists int i; 0 <= i && i < size; elem == arr[i]);
    //@ ensures \result == true;
    //@ also
    //@ public normal_behavior
    //@ requires size > 0;
    //@ requires (\forall int i; 0 <= i && i < size; elem != arr[i]);
    //@ ensures \result == false;
    public /* @ pure @*/ boolean contains(int elem) {
        for(int i = 0; i < size;i++){
        	if(arr[i]==elem){
        		return true;
        	}
        }
    	return false;
    }
    
    //@ public normal_behavior
    //@ requires size > 0;
    //@ ensures \result == arr[size-1];
    //@ assignable \nothing;
    //@also
    //@ requires size <= 0;
    //@ ensures \result == 0;
    public int max() {
        return size>0 ? arr[size-1] : 0;
    }

    //@ public normal_behavior
    //@ ensures \result == size;
    //@ assignable \nothing;
    public int getSize() {
        return size;
    }
    
    //@ public normal_behavior
    //@ ensures \result == capacity;
    //@ assignable \nothing;
    public int getCapacity() {
        return capacity;
    }
    //No JML
    public String toString() {
    	if(size > 0){
    		StringBuffer buffer = new StringBuffer();
        	buffer.append("[");
        	for(int i = 0; i < size-1;i++){
        		buffer.append(arr[i] + ", ");
        	}
        	buffer.append(arr[size-1]+"]");
        	return buffer.toString();
    	}else{
    		return "[empty]";
    	}
    }
}